es:ES, ff:FIFO, i:ff.C, e, e':{e:E| ff.R(i,e)} , j:ff.C.
(ff.S(j,i,ff.Sender(i,e)))
 (ff.S(j,i,ff.Sender(i,e')))
 ff.Sender(i,e) c ff.Sender(i,e')
 e c e' 

latex

Definitions	ff.R, ff.C, ff.S, ff.Sender, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), t.1, x. t(x), x.A(x), (state when e), P  Q, e c e', P & Q, s = t, Q  f P, for clients C sends FIFO   from j to i via (S[j,i],codes)   receives at i via (R[i],decodes), x:AB(x), x:A. B(x), x:A  B(x), {x:A| B(x)} , E, f(a), , Type, FIFO, x:A. B(x), t  T, ES, Q f P, (e < e'), b, A c B, P  Q, left + right
Lemmas	event system wf, FIFO wf, es-E wf, es-causle wf, es-state-when wf, antecedent-surjection wf, pi1 wf